A:Type, I:MaInterface(A), l:IdLnk, tg:Id, nmr:Namer(2;[tg; lname(l)] @ ma-interface-tags(I)).
Normal(A,I)
 gluable(I;l;tg)
 gluable2(A;I;l;tg)
 (interfaceGlue(A; I; l; tg; nmr)  Realizer) 

latex

Definitions

Realizer, interfaceGlue(A; I; l; tg; nmr), (L), xL.R(x), triggersGlue(A; l; tg; ds; conds), (link n from i to j), f(a), {i..j}, x:AB(x), left + right, State(ds), ma-interface-ds(I;i), x  dom(f), Top, Knd, t.2, f(x), [], type List, [car / cdr], filter(P;l), remove-repeats(eq;L), ma-interface-locs(I), x. t(x), x.A(x), (x  l), a < b, x:A. B(x), P  Q, t  T, s = t, gluable2(A;I;l;tg), gluable(I;l;tg), A, Normal(A,I), Normal(ds), Normal(T), Namer(n;Id_list), {x:A| B(x)} , Id, Atom$n, IdLnk, x:A  B(x), MaInterface(T), a:A fp B(a), b, Type

Lemmas

Rall wf, fpf-dom wf, assert wf, ma-interface-ds wf, mk lnk wf, triggersGlue wf, Rlist wf, interfaceGlue helper2, interfaceGlue helper